Nuprl Lemma : component-output-disjoint_wf 11,40
ds:(IdType{i}), da:(IdKndType{i}), A, B:Type{i}, Ca:component{i:l}(ds; da; A; Top),
Cb:component{i:l}
Cb:component(ds; da; B; Top).
component-output-disjoint{i:l}(ds; da; A; B; Ca; Cb)  {i'} 
latex

Definitionsx. t(x), P  Q, component-output-disjoint{i:l}(ds;da;T1;T2;C1;C2), , t  T, x:A. B(x), x(s), Component(ds;da;A;B)
LemmasKnd wf, Id wf, component wf, RealizerScheme wf, pi2 wf, abs-interface wf, top wf, es-interface-disjoint wf, es-decl wf, event system wf, interface wf

origin